<html>
<head><meta charset="utf-8"><title>Branding (&quot;generative types&quot;) in Rust · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html">Branding (&quot;generative types&quot;) in Rust</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="229129349"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/229129349" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#229129349">(Mar 06 2021 at 21:08)</a>:</h4>
<p>Some of you might find this recently submitted paper interesting. :)<br>
<a href="http://plv.mpi-sws.org/rustbelt/ghostcell/">http://plv.mpi-sws.org/rustbelt/ghostcell/</a></p>



<a name="229189696"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/229189696" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#229189696">(Mar 07 2021 at 14:00)</a>:</h4>
<p>Interesting! <br>
The distance between rustbelt and real rust still seems fairly big. Do you think a standardization initiative like Ferrocene could help?</p>



<a name="229200007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/229200007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Gwaihir Thorondorsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#229200007">(Mar 07 2021 at 16:33)</a>:</h4>
<p>Minor typo in the implementation: the doc comments for the <code>Send</code> and <code>Sync</code> <code>impl</code>s for <code>GhostCell</code> <a href="https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/ghostcell/src/lib.rs#L95-105">are swapped</a>.</p>



<a name="229200020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/229200020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Gwaihir Thorondorsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#229200020">(Mar 07 2021 at 16:34)</a>:</h4>
<p>Also, is there a reason why the <code>borrow</code> and <code>borrow_mut</code> methods are not implemented for all <code>T: ?Sized</code> types?</p>



<a name="229201417"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/229201417" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Gwaihir Thorondorsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#229201417">(Mar 07 2021 at 16:55)</a>:</h4>
<p>And I don't understand the choice of implementation for <code>InvariantLifetime</code>. Were it up to me, I would have chosen an implementation that only makes the parameter invariant and doesn't also disable <code>Send</code> and <code>Sync</code>. But then the bounds <code>for&lt;'id&gt; GhostToken&lt;'id&gt; : Send + Sync</code> and <code>for&lt;'id, T: Send&gt; GhostCell&lt;'id, T&gt; : Send</code> would be automatic and it is not clear to me whether this is a coincidence.</p>



<a name="230152960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230152960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230152960">(Mar 13 2021 at 10:11)</a>:</h4>
<p><span class="user-mention silent" data-user-id="369545">Gwaihir Thorondorsen</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust/near/229200007">said</a>:</p>
<blockquote>
<p>Minor typo in the implementation: the doc comments for the <code>Send</code> and <code>Sync</code> <code>impl</code>s for <code>GhostCell</code> <a href="https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/ghostcell/src/lib.rs#L95-105">are swapped</a>.</p>
</blockquote>
<p>good catch, thanks!</p>



<a name="230153007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230153007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230153007">(Mar 13 2021 at 10:12)</a>:</h4>
<p><span class="user-mention silent" data-user-id="369545">Gwaihir Thorondorsen</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust/near/229200020">said</a>:</p>
<blockquote>
<p>Also, is there a reason why the <code>borrow</code> and <code>borrow_mut</code> methods are not implemented for all <code>T: ?Sized</code> types?</p>
</blockquote>
<p>not really, we tend to not think much about unsized types^^ (and our formalization can't handle them)</p>



<a name="230153049"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230153049" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230153049">(Mar 13 2021 at 10:13)</a>:</h4>
<p><span class="user-mention silent" data-user-id="369545">Gwaihir Thorondorsen</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust/near/229201417">said</a>:</p>
<blockquote>
<p>And I don't understand the choice of implementation for <code>InvariantLifetime</code>. Were it up to me, I would have chosen an implementation that only makes the parameter invariant and doesn't also disable <code>Send</code> and <code>Sync</code>. But then the bounds <code>for&lt;'id&gt; GhostToken&lt;'id&gt; : Send + Sync</code> and <code>for&lt;'id, T: Send&gt; GhostCell&lt;'id, T&gt; : Send</code> would be automatic and it is not clear to me whether this is a coincidence.</p>
</blockquote>
<p>for <code>GhostCell</code>, there's an <code>UnsafeCell</code>, doesnt that kill Send+Sync?<br>
anyway I think explicit <code>Send</code>+<code>Sync</code> are always preferable. leaving it implicit <a href="https://www.ralfj.de/blog/2017/06/09/mutexguard-sync.html">quickly leads to bugs like this</a>.</p>



<a name="230153110"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230153110" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230153110">(Mar 13 2021 at 10:14)</a>:</h4>
<p>automatic Send/Sync makes a lot of sense in safe code, but once you write unsafe code with custom datatype invariants ("unsafe fields"), you <em>need</em> to think about whether that invariant does anything thread-local. explicit send/sync impls acknowledge that they do not.</p>



<a name="230153215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230153215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230153215">(Mar 13 2021 at 10:16)</a>:</h4>
<p><span class="user-mention silent" data-user-id="382207">Bas Spitters</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust/near/229189696">said</a>:</p>
<blockquote>
<p>Interesting! <br>
The distance between rustbelt and real rust still seems fairly big. Do you think a standardization initiative like Ferrocene could help?</p>
</blockquote>
<p>I think the largest chunk of work here is something that has to happen on the rustbelt side. ;) we have ideas for making lambda-rust more like MIR, but it turns out "places+values" ("lvalues +rvalues") make the type system a lot more complicated to state and we haven't reach a satisfactory formulation of that yet. also we should make our lifetime analysis closer to the borrow checker; I am putting a lot of hope into Polonious and its formalization via Oxide for that.</p>



<a name="230159159"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230159159" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230159159">(Mar 13 2021 at 12:19)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> Thanks. I had the impression that Oxide was a bit stalled. I'm happy that you're impression is different.<br>
We're working on verified extraction from Coq to rust, as part of <a href="https://github.com/AU-COBRA/ConCert">https://github.com/AU-COBRA/ConCert</a><br>
We need a reference saying that the "functional part" of rust satisfies weak CbV semantics. It should be "obvious", but I haven't seen it stated. Have you?</p>



<a name="230159325"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230159325" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230159325">(Mar 13 2021 at 12:22)</a>:</h4>
<p>I dont know the status of Oxide, indeed there hasn't been much news recently but I am still keeping my hopes up :)</p>



<a name="230160190"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230160190" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230160190">(Mar 13 2021 at 12:38)</a>:</h4>
<blockquote>
<p>We need a reference saying that the "functional part" of rust satisfies weak CbV semantics. It should be "obvious", but I haven't seen it stated. Have you?</p>
</blockquote>
<p>No I haven't. Given an imperative language semantics, how would one usually go about formally stating (and proving) this?</p>



<a name="230160871"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230160871" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Gwaihir Thorondorsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230160871">(Mar 13 2021 at 12:51)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust/near/230153049">said</a>:</p>
<blockquote>
<p>for <code>GhostCell</code>, there's an <code>UnsafeCell</code>, doesnt that kill Send+Sync?</p>
</blockquote>
<p>The <code>UnsafeCell&lt;T&gt;</code> <a href="https://doc.rust-lang.org/nightly/std/cell/struct.UnsafeCell.html#impl-Sync">definitely is <code>!Sync</code> for every <code>T</code></a>, but it <a href="https://doc.rust-lang.org/nightly/std/cell/struct.UnsafeCell.html#impl-Send">is <code>Send</code> whenever <code>T: Send</code></a>. Considering <code>UnsafeCell&lt;T&gt;</code> and <code>T</code> are the same <em>when owned</em>, I guess that makes sense. (I had the same reaction but went extra careful and checked the docs.)</p>



<a name="230160973"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230160973" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Gwaihir Thorondorsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230160973">(Mar 13 2021 at 12:52)</a>:</h4>
<p>The caution w.r.t. <code>Send</code> &amp; <code>Sync</code> in <code>unsafe</code> code makes sense; I guess I was just surprised the concerns weren't separated (which I now understand is just very nitpicky).</p>



<a name="230161445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230161445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230161445">(Mar 13 2021 at 13:01)</a>:</h4>
<p><span class="user-mention silent" data-user-id="369545">Gwaihir Thorondorsen</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust/near/230160973">said</a>:</p>
<blockquote>
<p>The caution w.r.t. <code>Send</code> &amp; <code>Sync</code> in <code>unsafe</code> code makes sense; I guess I was just surprised the concerns weren't separated (which I now understand is just very nitpicky).</p>
</blockquote>
<p>to be fair we didnt really think about it so deeply ;)</p>



<a name="230161505"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230161505" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230161505">(Mar 13 2021 at 13:02)</a>:</h4>
<p>I did not realize that <code>InvariantLifetime</code> kills Send+Sync because we weren't concerned with auto-deriving that anyway</p>



<a name="230560683"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230560683" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cjgillot <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230560683">(Mar 16 2021 at 17:52)</a>:</h4>
<p>I find unfortunate that we don't have a syntax to express <code>GhostToken::new</code> as returning a <code>GhostToken&lt;'id&gt;</code> for some unique non-unifiable lifetime <code>'id</code>. This would allow making this idiom easier to use.</p>



<a name="230560834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Branding%20%28%22generative%20types%22%29%20in%20Rust/near/230560834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Branding.20(.22generative.20types.22).20in.20Rust.html#230560834">(Mar 16 2021 at 17:53)</a>:</h4>
<p>yeah, being able to return a fresh lifetime would be nice. <code>fn foo() -&gt; exists&lt;'a&gt; T&lt;'a&gt;</code>...</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>